(declare-const x Int)
(assert (>= x 189))
(assert (<= x 290))
(assert (>= (+ x 3) 0))
(assert (< (+ x 3) 999))
(assert (>= (+ (* 2 x) 3) 0))
(assert (< (+ (* 2 x) 3) 999))
(assert (>= (- x 16) 0))
(assert (< (- x 16) 999))
(assert (>= (- (* 2 x) 16) 0))
(assert (< (- (* 2 x) 16) 999))
(check-sat)
